$\vdash$  ($\lambda$$A$,$r$,$z$. WellFnd\{i\}($A$;$x$,$y$.$r$($x$,$y$))) $\in$ $A$:Type$\rightarrow$($A$$\rightarrow$$A$$\rightarrow\mathbb{P}$)$\rightarrow$($\downarrow$True)$\rightarrow\mathbb{P}$'